Nuprl Lemma : comb_for_int_upper_wf
13,42
postcript
pdf
(
n
,
z
. {
n
...})
(
True)
Type
latex
Up
int
1
,
int
1
Definitions
t
T
,
,
x
:
A
.
B
(
x
)
,
T
Lemmas
true
wf
,
squash
wf
,
int
upper
wf
origin
n,z. {n...}) 
(
True)Type n,z. {n...}) (True)Type T
x:A. B(x)T